Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

PR summary b9242563f9

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

./scripts/reporting/technical-debt-metrics.sh pr_summary

The convention I like best says that a profunctor from C to D is a functor from C x D^op to types, or equally a functor from C to presheaves on D. This fits well with the analogy between profunctors and bimodules: a profunctor F from C to D is a family of types F d c with commuting "left" (aka covariant) actions by C and "right" (aka contravariant) actions by D. NB in Australia, it's common to call profunctors modules.

The one challenge with this convention is the ordering of variables in the object mapping F : D -> C -> Type. If in a profunctor from C to D you supply the variable from D first then you get to write F d c like I did above and this will match the intuitive ordering in examples derived from the hom bifunctor, where the contravariant argument appears first.

So these would be my concrete suggestions about conventions but others should of course weigh in too.

Let me suggest a few examples that should appear already in this file as a test of the API:

1. The construction of the hom profunctor from C to C.
2. For any functor F : C -> D the construction of a profunctor from C to D and the construction of a second profunctor from D to C.
3. The construction of the restriction of a profunctor from C to D along arbitrary functors H : A -> C and K : B -> D to get a profunctor from A to B. Note example 2 is obtained form example 1 in this way. To avoid the clutter of identity functors, you might want to formalize left restrictions, right restrictions, and two-sided restrictions.

Note these restrictions have a universal property that we can discuss if you like.

Thank you for taking your time to look at the code! I agree that the code will need some testing with examples and also some experimenting with automation, since it was fairly quick to write.

I am actually also working on a module with actions of functors on profunctors ("restrictions") which already contains all sorts of functoriality and action compatibility properties. This is needed for operads.

I can also add the hom profunctor and also a constructor for a profunctor on a pair of discrete categories (I need this too). For the hom profunctor, syncronizing with 'CategoryTheory.Functor.Hom' might also be important.

So there is a lot that can be added. Let me know how much of it would be a good amount for a first PR. Alternatively, this profunctors code can also be tested a bit in another repo (eventually including additional content like universal properties) to show that it works.

As you know, @adamtopaz and I are developing profunctors in a private repo. We have API analogous to yours and the glue to go back and forth between profunctors as the custom structure and as functors from C to presheaves on D. We found that the category theory automation worked sub-optimally in the category of types (this is well-known to the community) and decided to undertake the long overdue refactor of the category instance on types in #35060 before adding profunctors to mathlib. This is a pretty big task and I estimate that it is about halfway done. I would prefer it if we can wait for that and then we can coordinate on the development of profunctors in mathlib. What do you think?

@dagurtomas I'd love to hear more about the problems with the current category instance and how your refactor fixes it. When you have a momment could you explain or point me to a discussion on the zulip that I may have missed?

I guess the category of types specifically has not been discussed much publically on Zulip, but there have been discussions in the reviewer's channel (which was probably not the right place, there is nothing wrong with such discussions taking place in public). But really it's the same issue as with concrete categories in general (see e.g. #mathlib4 > Concrete category class redesign), and full subcategories, induced categories, etc.

When you have some type of objects and types of "morphisms" between them (say, groups and group homomorphisms), your instinct is to define a category structure on the type of groups, where the type G ⟶ H is defined as the type G →* H of group homomorphisms from G to H. But this instinct is wrong! It makes the category theory API interfere with the group theory API, and automation gets confused. Instead you define a one-field structure GrpCat.Hom, which gives you a layer of separation between the two API's.

This has been done now for all the standard concrete categories of algebraic structures and topological spaces. The same approach of one-field structures also works very well for e.g. full subcategories. Previously, the type of morphisms in the full subcategory was definitionally equal to the type of morphisms in the ambient category, but this tended to make automation confused. This has now also been refactored so that the hom set in the full subcategory is a one-field structure with the field being the hom set in tha ambient category. Because of how bad automation worked, the full subcategory API was rarely used before the refactor, e.g. the category of sheaves was defined as a custom structure with one-field structure homs instead of a full subcategory of presheaves. But earlier today, I delegated #36081 which relatively easily switched over to the full subcategory API.

Anyway, the category of types has been left unchanged, with X ⟶ Y definitionally equal to X → Y, but now we plan to introduce one-field structures there as well. We think that the refactor will require fixing about 400 files, which is probably the reason no one has attempted this before.

I am skeptical about the definition as a structure: I would favour defining profunctors as an abbrev for a category of bifunctors C ⥤ Dᵒᵖ ⥤ Type u.

Just using C ⥤ Dᵒᵖ ⥤ Type u actually was my first approach. Since I do not know enough about those automation issues, I decided to trust Adam and Dagur.

I would love to coordinate the development of profunctors! I contacted Adam some time ago so that we can do this, but he hasn't gotten around to replying.

I added some more stuff to the profunctors code on a separate repo.

There is a file in there on the hom profunctor and a file on actions of functors on profunctors, as discussed above.

Disclaimer: I'm experimenting with using AI for API design. Some of the code in there is WIP (mainly the code on cells) and needs some careful review and some refactoring. Some might say that using AI for this is a terrible idea, but so far I have been pleasantly surprised.

Can we remove the 'awaiting-author' label? I'm not sure that there is something that I need to do. If anything, we should agree on whether this is the right design of profunctors for mathlib or no.

Can we remove the 'awaiting-author' label? I'm not sure that there is something that I need to do. If anything, we should agree on whether this is the right design of profunctors for mathlib or no.

I would stand with my position that we should just use an abbrev for a category of (currified) bifunctors. The ongoing refactor of the category of Type is a good opportunity to make automation work fine.

Where is the refactor of Type taking place at the moment? Is it currently an obstacle to this PR?

#36613 is the refactor of the category of types

Now that the refactor of the category of types is merged, I've had some time to think about profunctors again. I think I agree with Joël now that we should just make Profunctor an abbrev for C ⥤ Dᵒᵖ ⥤ Type w. Otherwise we would need to duplicate too much API. The following code shows that automation works well, and that there is existing API for the three examples that @emilyriehl suggests:

import Mathlib.CategoryTheory.Yoneda

namespace CategoryTheory

open Opposite

universe w

variable (C D : Type*) [Category* C] [Category* D]

@[pp_with_univ]
structure ProfunctorCore where
  obj : C → D → Type w
  map {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y') : obj X Y' ⟶ obj X' Y
  map_id (X : C) (Y : D) : map (𝟙 X) (𝟙 Y) = 𝟙 _ := by cat_disch
  map_comp {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : D} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃) :
    map (f ≫ f') (g ≫ g') = map f g' ≫ map f' g := by cat_disch

attribute [local simp] ProfunctorCore.map_id ProfunctorCore.map_comp

variable {C D}

@[local simp]
lemma ProfunctorCore.map_id_comp (P : ProfunctorCore.{w} C D) (X : C) {Y Y' Y'' : D}
    (g : Y ⟶ Y') (g' : Y' ⟶ Y'') :
    P.map (𝟙 X) (g ≫ g') = P.map (𝟙 X) g' ≫ P.map (𝟙 X) g := by
  nth_rw 1 [← Category.id_comp (𝟙 X)]
  simp only [P.map_comp]

@[local simp]
lemma ProfunctorCore.map_comp_id (P : ProfunctorCore.{w} C D) {X X' X'' : C} (Y : D)
    (f : X ⟶ X') (f' : X' ⟶ X'') :
    P.map (f ≫ f') (𝟙 Y) = P.map f (𝟙 Y) ≫ P.map f' (𝟙 Y) := by
  nth_rw 1 [← Category.id_comp (𝟙 Y)]
  simp only [P.map_comp]

@[reassoc (attr := local simp)]
lemma ProfunctorCore.map_lid_comp_map_rid (P : ProfunctorCore.{w} C D) {X X' : C} {Y Y' : D}
    (f : X ⟶ X') (g : Y ⟶ Y') : P.map (𝟙 _) g ≫ P.map f (𝟙 _) = P.map f g := by
  simp [← P.map_comp]

@[reassoc (attr := local simp)]
lemma ProfunctorCore.map_rid_comp_map_lid (P : ProfunctorCore.{w} C D) {X X' : C} {Y Y' : D}
    (f : X ⟶ X') (g : Y ⟶ Y') : P.map f (𝟙 _) ≫ P.map (𝟙 _) g = P.map f g := by
  simp [← P.map_comp]

variable (C D) in
/--
A profunctor from C to D is a bifunctor `D^op × C -> Type`. We define it in its curried form,
i.e. as `C ⥤ Dᵒᵖ ⥤ Type`.
-/
@[pp_with_univ]
abbrev Profunctor := C ⥤ Dᵒᵖ ⥤ Type w

@[simps]
def Profunctor.ofCore (P : ProfunctorCore.{w} C D) : Profunctor.{w} C D where
  obj X := { obj Y := P.obj X (unop Y), map f := P.map (𝟙 _) f.unop }
  map g := { app X := P.map g (𝟙 _) }

abbrev Profunctor.obj₂ (P : Profunctor.{w} C D) (X : C) (Y : D) : Type w := (P.obj X).obj (op Y)

abbrev Profunctor.map₂ (P : Profunctor.{w} C D) {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y') :
    P.obj₂ X Y' ⟶ P.obj₂ X' Y := (P.map f).app (op Y') ≫ (P.obj X').map g.op

lemma Profunctor.map₂_def (P : Profunctor.{w} C D) {X X' : C} {Y Y' : D} (f : X ⟶ X')
    (g : Y ⟶ Y') : P.map₂ f g = (P.map f).app (op Y') ≫ (P.obj X').map g.op :=
  rfl

lemma Profunctor.map₂_naturality_symm (P : Profunctor.{w} C D) {X X' : C} {Y Y' : D} (f : X ⟶ X')
    (g : Y ⟶ Y') : P.map₂ f g = (P.obj X).map g.op ≫ (P.map f).app (op Y) := by
  simp

lemma Profunctor.map_lid_comp_map_rid_apply (P : Profunctor.{w} C D) {X X' : C} {Y Y' : D}
    (f : X ⟶ X') (g : Y ⟶ Y') (x : P.obj₂ X Y') :
    P.map₂ f (𝟙 _) (P.map₂ (𝟙 _) g x) = P.map₂ f g x := by
  simp

lemma Profunctor.map_rid_comp_map_lid_apply (P : Profunctor.{w} C D)
    {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y') (x : P.obj₂ X Y') :
    P.map₂ (𝟙 _) g (P.map₂ f (𝟙 _) x) = P.map₂ f g x := by
  simp

example : Category (Profunctor.{w} C D) := inferInstance

example (P : Cᵒᵖ ⥤ D ⥤ Type w) : Profunctor.{w} D C := P.flip

@[simps! obj_obj obj_map map_app]
protected def Profunctor.yoneda : Profunctor C C := yoneda

def Profunctor.op (P : Profunctor.{w} C D) : Profunctor.{w} Dᵒᵖ Cᵒᵖ :=
  .ofCore {
    obj X Y := P.obj₂ (Opposite.unop Y) (Opposite.unop X)
    map f g := P.map₂ g.unop f.unop }

@[simps! obj_obj obj_map map_app]
def Profunctor.whiskeringLeft {A B : Type*} [Category* A] [Category* B]
    (P : Profunctor.{w} C D) (F : A ⥤ C) (G : B ⥤ D) : Profunctor.{w} A B :=
  (((Functor.whiskeringLeft₂ _).obj F).obj G.op).obj P

@[simps! obj_obj obj_map map_app]
def Functor.toProfunctor (F : C ⥤ D) : Profunctor C D :=
  (Profunctor.yoneda (C := D)).whiskeringLeft F (𝟭 _)

@[simps! obj_obj obj_map map_app]
def Functor.toProfunctorFlip (F : C ⥤ D) : Profunctor D C :=
  (Profunctor.yoneda (C := D)).whiskeringLeft (𝟭 _) F

end CategoryTheory

Here is a quick definition of profunctor composition using the code above:

universe w v u

variable {C : Type*} {D : Type w} {E : Type*} [Category* C] [Category* D] [Category* E]

inductive Profunctor.compRel (F : Profunctor.{v} C D)
    (G : Profunctor.{u} D E) (X : C) (Y : E) :
    (W : D) × F.obj₂ X W × G.obj₂ W Y → (W : D) × F.obj₂ X W × G.obj₂ W Y → Prop where
  | mk {W W' : D} (f : W ⟶ W') (x : F.obj₂ X W') (y : G.obj₂ W Y) :
    compRel F G X Y ⟨_, (F.map₂ (𝟙 X) f) x, y⟩ ⟨_, x, (G.map₂ f (𝟙 Y)) y⟩

def Profunctor.comp (F : Profunctor.{v} C D) (G : Profunctor.{u} D E) :
    Profunctor.{max u v w} C E := .ofCore {
  obj X Y := Quot <| Profunctor.compRel F G X Y
  map f g := TypeCat.ofHom (fun x ↦ x.liftOn
      (fun ⟨W, a, b⟩ ↦ .mk _ ⟨W, (F.map₂ f (𝟙 _)) a, (G.map₂ (𝟙 _) g) b⟩) <| by
    rintro ⟨W, a, b⟩ ⟨W', a', b'⟩ ⟨h, x, y⟩
    apply Quot.sound
    have : F.compRel G _ _ ⟨W, ((F.map₂ f (𝟙 W') ≫ F.map₂ (𝟙 _) h) a', (G.map₂ (𝟙 W) g) b)⟩
        ⟨W', ((F.map₂ f (𝟙 W')) a', (G.map₂ (𝟙 W) g ≫ G.map₂ h (𝟙 _)) b)⟩ :=
      ⟨h, (F.map₂ f (𝟙 _)) a', (G.map₂ (𝟙 _) g) b⟩
    simpa using this)
  map_id _ _ := by ext ⟨⟩; simp
  map_comp _ _ _ _ := by ext ⟨⟩; simp }

However, the correct way to go is to define explicit coends in the category of types and use that for the definition of composition. I'm working on this

Thanks for your work on this @adrianmartir ! I see that there is now a separate PR that implements profunctors (#38085), which also accounts for @joelriou 's comments, and it seems that you are listed as a coauthor on the file from that PR. I will therefore close this PR, and assume that further work on profunctors takes place in #38085.

I'm happy to see that getting profunctors into mathlib is progressing :)

@dagurtomas , I'm not sure that using coends here is really better, since the quotient construction is more explicit. I've been also doing something really similar when formalizing operads. First, I defined a profunctor, which on objects X and Y is given by (W : D) × F.obj₂ X W × G.obj₂ W Y and then defined a similar quotient relation on it. This then makes it fairly transparent to define natural transformations out of the functor tensor product by using the universal property of the quotient, i.e. by checking that the map is compatible with the two actions on W. This is in analogy to how one first constructs a bilinear map and only then the map out of the tensor product.

The quotient relation just states what a compatible map really is.

Of course, in the end, this universal property is the same as the universal property of the coend and both constructions are non-computable, but I would argue that the coend is less transparent and I also think it's less useful for the purposes I had in mind.

Here is the n-ary version of the profunctor tensor product that I defined based on an inductive quotient relation.

I agree we need to be explicit here, which is why I'm defining explicit coends in Type in #38086. The quotient of this relation is the coend in Type.

Do you already have the bicategory structure on your ProfCat?